OP
←(V1,A1)
NIL
NIL
NIL
ISVAR(V1);;
C(V1,A1);;

ITERATIVE
TGCD
NIL
NIL
NIL
NEWVAR(Y1);>(X,(0)); >(Y,(0));C(X1,X);C(Y1,Y);;
C(X1,V1);C(Y1,V2);VGCD(V1 V2 V3);VGCD(X,Y,V3);;
VGCD(V1,V2,V4);VGCD(E1,E2,V4);>((PLUS V1 V2),(PLUS E1 E2));C(X1,E1);C(Y1,E2);;
NIL
C(X1,(GCD X,Y));;
C(X1,(GCD X,Y));;

DEF
REDUCE
NIL
NIL
NIL
=(E2,V2);=(E1,(MINUS V1,W));>(W,(0));;
>((PLUS V1,V2),(PLUS E1,E2));;

AXIOM
TGCD1
NIL
NIL
NIL
VGCD((MINUS B,C),C,A);;
VGCD(B,C,A);;

AXIOM
TGCD2
NIL
NIL
NIL
VGCD(B,C,A);;
VGCD(C B A);;

NIL
NIL

INTEGER(X); INTEGER(Y);
>(X,(0)); >(Y,(0)); ISVAR(X1);VGCD(X,Y,(GCD X,Y));;

T

((C T NIL NIL (X,*))
(> T NIL NIL NIL)
(= T NIL NIL NIL) 
(VGCD T NIL NIL NIL) 
(CGCD T NIL NIL NIL) 
(INTEGER NIL NIL NIL NIL)
               )

T
((ADD1(X)(/( X/+ 1 /) ))
 (SUB1(X)(/( X/- 1 /) ))
 (PLUS(X Y)( /(X /+ Y/)) ) )